module sva_ca_implication_2;
    logic clk;
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    logic a, b;
    initial begin
        a=1; b=1; #5;
        a=1; b=0; #10;
        a=1; b=1; #10;
        a=1; b=1; #10;
        a=0; b=0; #10;
        a=1; b=1; #10;
        $finish;
    end

    // |-> 为 Overlapped Implication
    // a |-> b 的含义: 当 a 在时钟沿 N 为真时, b 也必须在同一个时钟沿 N 为真;
    // a |=> ##2 b 的含义: 如果 a 在周期 N 为真，那么从下一个周期 N+1 开始数2个周期，即在周期 N+3 b 必须为真
    property p1;
        @(posedge clk) a |-> b;
    endproperty
    ap1: assert property(p1) $info("ap1 passed"); else $error("ap1 failed");

    // |=> 为 Non-overlapped Implication
    // a |=> b 的含义: 当 a 在时钟沿 N 为真时, b 必须在下一个时钟沿 N+1 为真; a |=> b 和 a |-> ##1 b 是完全等价的.
    // a |-> ##2 b 的含义: 如果 a 在周期 N 为真, 那么从周期 N 开始数 2 个周期, 即在周期 N+2 b 必须为真

    property p2;
        @(posedge clk) a |=> b;
    endproperty
    ap2: assert property(p2) $info("ap2 passed"); else $error("ap2 failed");

    initial begin
        $dumpfile("dump.vcd"); $dumpvars;
    end
endmodule

/* Output: QuestaSim
# ** Info: ap1 passed
#    Time: 5 ns Started: 5 ns  Scope: sva_ca_implication_2.ap1 File: sva_ca_implication_2.sv Line: 25
# ** Error: ap2 failed
#    Time: 15 ns Started: 5 ns  Scope: sva_ca_implication_2.ap2 File: sva_ca_implication_2.sv Line: 34
# ** Error: ap1 failed
#    Time: 15 ns Started: 15 ns  Scope: sva_ca_implication_2.ap1 File: sva_ca_implication_2.sv Line: 25
# ** Info: ap2 passed
#    Time: 25 ns Started: 15 ns  Scope: sva_ca_implication_2.ap2 File: sva_ca_implication_2.sv Line: 34
# ** Info: ap1 passed
#    Time: 25 ns Started: 25 ns  Scope: sva_ca_implication_2.ap1 File: sva_ca_implication_2.sv Line: 25
# ** Info: ap2 passed
#    Time: 35 ns Started: 25 ns  Scope: sva_ca_implication_2.ap2 File: sva_ca_implication_2.sv Line: 34
# ** Info: ap1 passed
#    Time: 35 ns Started: 35 ns  Scope: sva_ca_implication_2.ap1 File: sva_ca_implication_2.sv Line: 25
# ** Error: ap2 failed
#    Time: 45 ns Started: 35 ns  Scope: sva_ca_implication_2.ap2 File: sva_ca_implication_2.sv Line: 34
 */